$\forall$$p$:FinProbSpace, $a$, $b$:Atom2, $C$:p{-}open($p$).
\\[0ex]measure($C$) = 1 $\Rightarrow$ ($C$:p{-}open($p$)$\parallel$$a$ $\vee$ $C$:p{-}open($p$)$\parallel$$b$) $\Rightarrow$ ($\exists$$n$:$\mathbb{N}$. ($C$($<$$n$, random($p$;$a$;$b$)$>$) = 1))